YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { f(a, empty()) -> g(a, empty())
  , f(a, cons(x, k)) -> f(cons(x, a), k)
  , g(empty(), d) -> d
  , g(cons(x, k), d) -> g(k, cons(x, d)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  none
TcT has computed following constructor-restricted linear polynomial
interpretation.
     [empty]() = 2          
                            
   [f](x1, x2) = 2*x1 + 3*x2
                            
   [g](x1, x2) = 2*x1 + x2  
                            
[cons](x1, x2) = 1 + x1 + x2
                            

This order satisfies following ordering constraints

     [f(a, empty())] = 2*a + 6            
                     > 2*a + 2            
                     = [g(a, empty())]    
                                          
  [f(a, cons(x, k))] = 2*a + 3 + 3*x + 3*k
                     > 2 + 2*x + 2*a + 3*k
                     = [f(cons(x, a), k)] 
                                          
     [g(empty(), d)] = 4 + d              
                     > d                  
                     = [d]                
                                          
  [g(cons(x, k), d)] = 2 + 2*x + 2*k + d  
                     > 2*k + 1 + x + d    
                     = [g(k, cons(x, d))] 
                                          

Hurray, we answered YES(?,O(n^1))